Inference at * 1 2 1 2 1 
Iof proof for Lemma adjacent-append:



1. T : Type
2. x : T
3. y : T
4. L1 : T List
5. L2 : T List
6. i : {0..((||L1||+||L2||) - 1)}
7. x = (L1 @ L2)[i]
8. y = (L1 @ L2)[(i+1)]
9. (i < ||L1||)
  y = L2[((i - ||L1||)+1)] 

latex

 by ((RWO "select_append_back" (-2)) 
CollapseTHEN (((Auto') 
CollapseTHEN (((NthHypSq (-2)) 

CoCollapseTHEN ((if (((first_nat 2:n)) = 0) then (Repeat (((EqCD) 
CollapseTHEN ((Try (Trivial))
C)))) else (RepeatFor (first_nat 2:n) (((EqCD) 
CollapseTHEN ((Try (Trivial)))))))))))))
Co

latex

C1: 

C1: 8. y = L2[((i+1) - ||L1||)]
C1: 9. (i < ||L1||)
C1:   ((i - ||L1||)+1) ~ ((i+1) - ||L1||)
C.

Definitions	P  Q, P & Q, x:A  B(x), P  Q, P  Q, n+m, n - m, #$n, l[i], as @ bs, {x:A| B(x)} , , ||as||, i  j , x:A. B(x), x:AB(x), A, s = t, {i..j}, type List, s ~ t, Type
Lemmas	iff wf, rev implies wf, select append back